Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(map,f),nil)  → nil
2:    app(app(map,f),app(app(cons,x),xs))  → app(app(cons,app(f,x)),app(app(map,f),xs))
3:    app(flatten,app(app(node,x),xs))  → app(app(cons,x),app(concat,app(app(map,flatten),xs)))
4:    app(concat,nil)  → nil
5:    app(concat,app(app(cons,x),xs))  → app(app(append,x),app(concat,xs))
6:    app(app(append,nil),xs)  → xs
7:    app(app(append,app(app(cons,x),xs)),ys)  → app(app(cons,x),app(app(append,xs),ys))
There are 15 dependency pairs:
8:    APP(app(map,f),app(app(cons,x),xs))  → APP(app(cons,app(f,x)),app(app(map,f),xs))
9:    APP(app(map,f),app(app(cons,x),xs))  → APP(cons,app(f,x))
10:    APP(app(map,f),app(app(cons,x),xs))  → APP(f,x)
11:    APP(app(map,f),app(app(cons,x),xs))  → APP(app(map,f),xs)
12:    APP(flatten,app(app(node,x),xs))  → APP(app(cons,x),app(concat,app(app(map,flatten),xs)))
13:    APP(flatten,app(app(node,x),xs))  → APP(cons,x)
14:    APP(flatten,app(app(node,x),xs))  → APP(concat,app(app(map,flatten),xs))
15:    APP(flatten,app(app(node,x),xs))  → APP(app(map,flatten),xs)
16:    APP(flatten,app(app(node,x),xs))  → APP(map,flatten)
17:    APP(concat,app(app(cons,x),xs))  → APP(app(append,x),app(concat,xs))
18:    APP(concat,app(app(cons,x),xs))  → APP(append,x)
19:    APP(concat,app(app(cons,x),xs))  → APP(concat,xs)
20:    APP(app(append,app(app(cons,x),xs)),ys)  → APP(app(cons,x),app(app(append,xs),ys))
21:    APP(app(append,app(app(cons,x),xs)),ys)  → APP(app(append,xs),ys)
22:    APP(app(append,app(app(cons,x),xs)),ys)  → APP(append,xs)
The approximated dependency graph contains one SCC: {8,10-12,14,15,17,19,21}.
Tyrolean Termination Tool  (42.38 seconds)   ---  May 3, 2006